#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 110
for i in range(0,maxPrio):
  rank.append([])

# SOURCES AND REUSE LEMMAS

if lemma == "sqn_ue_invariance" or \
     lemma == "sqn_hss_invariance" or \
     lemma == "sqn_ue_src" or \
     lemma == "sqn_hss_src":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*Sqn_UE\(.*', line): rank[90].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[90].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[95].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[95].append(num)

elif lemma == "sqn_ue_nodecrease":
  for line in lines:
    num = line.split(':')[0]    
    if re.match('.*\(last\(#j.*', line): rank[100].append(num)
    elif re.match('.*Sqn_UE_Change\(.*', line): rank[90].append(num)
    elif re.match('.*\(#vr < #i\).*', line): rank[80].append(num)
    elif re.match('.*Sqn_UE\(.*count.1.*', line): rank[70].append(num)

# SECRECY LEMMAS

elif lemma == "secrecy_ue_kseaf_noKeyRev_noSupiRev_noSqnRev_noAsyKeyRev":
  for line in lines:
    num = line.split(':')[0]   
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[96].append(num)
    elif re.match('.*~~>*', line): rank[96].append(num)
    elif re.match('.*St_.*\(.*', line): rank[90].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[30].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[30].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[20].append(num)
    elif re.match('.*RcvS\(.*', line): rank[10].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[9].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[8].append(num)
    elif re.match('.*Sec\(.*', line): rank[7].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[5].append(num)
    elif re.match('.*!KU\( pk\(.*', line): rank[4].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[3].append(num)

elif "secrecy_ue_kseaf" in lemma:
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[96].append(num)
    elif re.match('.*~~>*', line): rank[96].append(num)
    elif re.match('.*St_.*\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[80].append(num)
    elif re.match('.*RcvS\(.*', line): rank[75].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[60].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[30].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[30].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( pk\(.*', line): rank[18].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[15].append(num)

elif "secrecy_ue_supi" in lemma:
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[96].append(num)
    elif re.match('.*=.*=.*=.*', line): rank[96].append(num)
    elif re.match('.*~~>*', line): rank[96].append(num)
    elif re.match('.*St_.*\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[80].append(num)
    elif re.match('.*RcvS\(.*\'aia\'.*', line): rank[75].append(num)
    elif re.match('.*RcvS\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[60].append(num)
    elif re.match('.*!KU\( f1\(KDF\(KDF\(.*', line): rank[60].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[60].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[45].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[40].append(num)

elif ("secrecy_hss" in lemma and not "_k_" in lemma) or \
     ("secrecy_seaf" in lemma and not "_k_" in lemma):
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[96].append(num)
    elif re.match('.*=.*=.*=.*', line): rank[96].append(num)
    elif re.match('.*~~>*', line): rank[96].append(num)
    elif re.match('.*St_.*\(.*', line): rank[90].append(num)
    elif re.match('.*Sec\(.*', line): rank[90].append(num)
    elif "_noChanRevAtAll_noSupiRev_noAsyKeyRev" in lemma and re.match('.*!KU\( ~supi.*', line): rank[80].append(num)
    elif ("seaf" in lemma and re.match('.*!KU\( KDF\(.*', line)): rank[60].append(num)
    elif (not ("noChanRev_noKeyRev" in lemma) and re.match('.*Sqn_UE\(.*', line)): rank[50].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[49].append(num)
    elif (not ("noChanRev_noKeyRev" in lemma) and re.match('.*Sqn_HSS\(.*', line)): rank[48].append(num)
    elif re.match('.*RcvS\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( SHA256\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[30].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[25].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( pk\(.*', line): rank[18].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[15].append(num)
    else: rank[0].append(num)

# AGREEMENTS LEMMAS

elif lemma == "weakagreement_hss_ue_noAsyKeyRev_noSupiRev_noSqnRev_noChanRev" or \
     lemma == "noninjectiveagreement_hss_ue_snname_noKeyRev" or \
     lemma == "weakagreement_hss_seaf_noAsyKeyRev_noSupiRev_noSqnRev_noKeyRev" or \
     lemma == "noninjectiveagreement_hss_seaf_supi_noRev" or \
     lemma == "noninjectiveagreement_hss_ue_supi_noKeyRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[96].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*St_1_SEAF\(.*', line): rank[95].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*Sec\( .*', line): rank[95].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*~~>.*', line): rank[94].append(num)
    elif (("weak" in lemma) or ("hss_seaf" in lemma)) and \
	 re.match('.*Sqn_HSS\(.*', line): rank[90].append(num)
    elif (("weak" in lemma) or ("hss_seaf" in lemma)) and \
	 re.match('.*Sqn_UE\(.*', line): rank[90].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[69].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*!KU\( f1\(~k.*', line): rank[66].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*!KU\( \(f5\(~k.*', line): rank[63].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*!KD\( \(f5\(~k.*', line): rank[63].append(num)
    elif ("hss_seaf" in lemma) and \
	 re.match('.*!KU\( ~sqn.*', line): rank[62].append(num)
    elif re.match('.*RcvS\(.*\'ac\'.*', line): rank[60].append(num)
    elif re.match('.*RcvS\(.*\'aia\'.*', line): rank[55].append(num)
    elif re.match('.*RcvS\(.*\'air\'.*', line): rank[50].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[45].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[40].append(num)

elif lemma == "injectiveagreement_ue_hss_autn_noKeyRev" or \
     lemma == "noninjectiveagreement_ue_hss_supi_noKeyRev" or \
     lemma == "injectiveagreement_hss_ue_kseaf_noKeyRev" or \
     lemma == "injectiveagreement_hss_ue_kseaf_noRestr":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( KDF\(<f3.*', line): rank[41].append(num)
    elif re.match('.*RcvS\(.*<\'ac\'.*', line): rank[40].append(num)

elif lemma == "cleanAttack_injectiveagreement_ue_hss_supi_noRev" or \
     lemma == "cleanAttack_injectiveagreement_ue_hss_keyConf_supi_noRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line) or \
	 re.match('.*!KU\( f3\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[85].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(<f3.*', line): rank[83].append(num)
    elif re.match('.*\(#.*= #.*\).*\(#.*= #.*\).*\(#.*= #.*\).*', line): rank[82].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[81].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[81].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[80].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[79].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[70].append(num)
    elif re.match('.*~~.*', line): rank[66].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[65].append(num)
    elif re.match('.*!KU\( f1\(~.*', line): rank[65].append(num)
    elif re.match('.*RcvS\(.*', line): rank[62].append(num)
    elif re.match('.*!KU\( \(f5\(~k,.*', line): rank[61].append(num)
    elif re.match('.*!KD\( \(f5\(~k,.*', line): rank[61].append(num)
    elif re.match('.*!KU\( f1\(K.*', line): rank[60].append(num)
    elif re.match('.*!KU\( ~RAND.*', line): rank[50].append(num)

elif lemma == "injectiveagreement_ue_hss_kseaf_keyConf_noKeyRev" or \
     lemma == "noninjectiveagreement_ue_hss_keyConf_supi_noKeyRev" or \
     lemma == "noninjectiveagreement_ue_hss_snname_keyConf_noKeyRev" or \
     lemma == "noninjectiveagreement_ue_hss_kseaf_keyConf_noRestr":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( f2\(.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[97].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[97].append(num)
    elif re.match('.*Commit\(.*', line): rank[96].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[96].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[95].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[95].append(num)
    elif re.match('.*St_4_SEAF\(.*', line): rank[95].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[95].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[95].append(num)
    elif re.match('.*!KU\( f1\(KDF\(KDF\(.*', line): rank[85].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(.*', line): rank[85].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[85].append(num)
    elif re.match('.*RcvS\(.*<\'aia\'.*', line): rank[70].append(num)

elif lemma == "injectiveagreement_hss_seaf_kseaf_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_ue_kseaf_noRestr":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[70].append(num)
    elif re.match('.*RcvS\(.*', line): rank[65].append(num)

elif lemma == "weakagreement_ue_hss_noAsyKeyRev_noSupiRev_noSqnRev_noChanRev" or \
     lemma == "weakagreement_ue_hss_keyConf_noAsyKeyRev_noSupiRev_noSqnRev_noChanRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[97].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[70].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( \(f5\(~k,.*', line): rank[69].append(num)
    elif re.match('.*!KU\( f5\(.*', line): rank[69].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[69].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[69].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[69].append(num)
    elif re.match('.*!KU\( f1\(~.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f1\(K.*', line): rank[45].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(.*', line): rank[43].append(num)
    elif re.match('.*!KU\( KDF\(<f3.*', line): rank[43].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( ~sqn_roo.*', line): rank[40].append(num)

elif lemma == "weakagreement_ue_seaf_keyConf_noRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[89].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[88].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[88].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[87].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(<f3\(.*', line): rank[87].append(num)
    elif re.match('.*!KU\( f1\(KDF\(KDF\(<f3\(~k.*', line): rank[87].append(num)
    elif re.match('.*!KU\( f3\(~k*', line) : rank[87].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[84].append(num)
    elif re.match('.*St_1_SEAF\(.*', line): rank[84].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[84].append(num)
    elif re.match('.*~~>.*', line): rank[80].append(num)
    elif re.match('.*RcvS\( ~idSN.*', line): rank[47].append(num)
    elif re.match('.*RcvS\(.*', line): rank[46].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[45].append(num)
    elif re.match('.*!Ltk_Sym\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[30].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[25].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[25].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[22].append(num)
    elif re.match('.*!KU\( ~RAN.*', line): rank[20].append(num)
    elif re.match('.*!KU\( ~sup.*', line): rank[10].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[8].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[6].append(num)
    elif re.match('.*!KU\( ~sup.*', line): rank[5].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[4].append(num)

elif lemma == "weakagreement_ue_seaf_noRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[85].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[84].append(num)
    elif re.match('.*St_2_UE\(.*', line): rank[84].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[84].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[84].append(num)
    elif re.match('.*~~>.*', line): rank[80].append(num)
    elif re.match('.*RcvS\( ~idSN.*', line): rank[47].append(num)
    elif re.match('.*RcvS\(.*', line): rank[46].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[45].append(num)
    elif re.match('.*!Ltk_Sym\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( f4\(.*', line): rank[30].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[25].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[25].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[22].append(num)
    elif re.match('.*!KU\( ~RAN.*', line): rank[20].append(num)
    elif re.match('.*!KU\( ~sup.*', line): rank[10].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[8].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[6].append(num)
    elif re.match('.*!KU\( ~sup.*', line): rank[5].append(num)
    elif re.match('.*!KU\( ~sk.*', line): rank[4].append(num)

elif lemma == "weakagreement_seaf_ue_noKeyRev_noChanRev" or \
     lemma == "weakagreement_seaf_ue_KeyConf_noKeyRev_noChanRev" or \
     lemma == "weakagreement_seaf_ue_noAsyKeyRev_noSupiRev_noSqnRev_noChanRev" or \
     lemma == "weakagreement_seaf_ue_KeyConf_noAsyKeyRev_noSupiRev_noSqnRev_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_ue_supi_noKeyRev_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_ue_keyConf_supi_noKeyRev_noChanRev" or \
     lemma == "cleanAttack_injectiveagreement_seaf_ue_supi_noRev" or \
     lemma == "weakagreement_seaf_ue_KeyConf_noKeyRev_noAsyKeyRev_noSupiRev_noSqnRev" or \
     lemma == "weakagreement_seaf_ue_noKeyRev_noAsyKeyRev_noSupiRev_noSqnRev":


  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif ("noSqnRev" in lemma or "noRev" in lemma) and \
        (re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line)): rank[85].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[84].append(num)
    elif re.match('.*~~.*', line): rank[80].append(num)
    elif re.match('.*=.*=.*=.*', line): rank[80].append(num)
    elif re.match('.*Commit\(.*', line): rank[79].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[79].append(num)
    elif re.match('.*St_4_SEAF\(.*', line): rank[79].append(num)
    elif re.match('.*RcvS\(.*<\'aca\'.*', line): rank[62].append(num)
    elif re.match('.*RcvS\(.*<\'ac\'.*', line): rank[61].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(<.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[40].append(num)
    elif re.match('.*RcvS\(.*<\'aia\'.*', line): rank[30].append(num)
    elif re.match('.*RcvS\(.*<\'air\'.*', line): rank[29].append(num)
    elif re.match('.*!KU\( \(f5\(~k.*', line): rank[28].append(num)
    elif re.match('.*!KD\( \(f5\(~k.*', line): rank[28].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[25].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[25].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( pk\(.*', line): rank[18].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[15].append(num)
    elif re.match('.*!KU\( f1\(~.*', line): rank[12].append(num)
    elif re.match('.*!KU\( f1\(K.*', line): rank[11].append(num)
    else : rank[0].append(num)

elif lemma == "noninjectiveagreement_seaf_ue_kseaf_noRev" or \
     lemma == "noninjectiveagreement_seaf_ue_kseaf_keyConf_noRev" or \
     lemma == "cleanAttack_noninjectiveagreement_seaf_ue_kseaf_keyConf_noRev" or \
     lemma == "cleanAttack_noninjectiveagreement_seaf_ue_kseaf_noRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif "noRev" in lemma and \
        (re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line)): rank[85].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[84].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(<f3\(.*', line): rank[82].append(num)
    elif (not lemma == "cleanAttack_noninjectiveagreement_seaf_ue_kseaf_keyConf_noRev" and \
        re.match('.*=.*=.*=.*', line)): rank[81].append(num)
    elif re.match('.*Commit\(.*', line): rank[80].append(num)
    elif re.match('.*~~>.*', line): rank[80].append(num)
    elif re.match('.*St_4_SEAF\(.*', line): rank[79].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[79].append(num)
    elif re.match('.*RcvS\(.*<\'aia\'.*', line): rank[78].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[77].append(num)
    elif re.match('.*RcvS\(.*<\'air\'.*', line): rank[76].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(.*', line): rank[75].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[74].append(num)
    elif re.match('.*!KU\( ~RAND.*', line): rank[73].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[72].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[71].append(num)
    elif re.match('.*!KD\( \(f5\(.*', line): rank[70].append(num)
    elif re.match('.*St_1_SEAF\(.*', line): rank[69].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[67].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[66].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[65].append(num)
    elif re.match('.*!KU\( ~idHN.*', line): rank[64].append(num)
    elif re.match('.*!KU\( ~idSN.*', line): rank[63].append(num)
    elif re.match('.*RcvS\(.*<\'aca\'.*', line): rank[62].append(num)
    elif re.match('.*RcvS\(.*<\'ac\'.*', line): rank[61].append(num)

elif lemma == "injectiveagreement_seaf_hss_kseaf_noRev" or \
     lemma == "weakagreement_seaf_hss_noAsyKeyRev_noSupiRev_noSqnRev_noKeyRev" or \
     lemma == "weakagreement_seaf_hss_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_hss_RESSTAR_noChanRev" or \
     lemma == "injectiveagreement_seaf_hss_kseaf_noKeyRev_noChanRev" or \
     lemma == "injectiveagreement_seaf_hss_kseaf_keyConf_noKeyRev_noChanRev" or \
     lemma == "weakagreement_seaf_hss_keyConf_noAsyKeyRev_noSupiRev_noSqnRev_noKeyRev" or \
     lemma == "noninjectiveagreement_seaf_hss_keyConf_supi_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_hss_kseaf_keyConf_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_hss_supi_noChanRev" or \
     lemma == "noninjectiveagreement_seaf_hss_kseaf_noChanRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( f3\(~k,.*', line) : rank[95].append(num)
    elif re.match('.*!KU\( f5\(~k,.*', line) : rank[95].append(num)
    elif re.match('.*St_3_SEAF\(.*', line) : rank[80].append(num)
    elif re.match('.*!KU\( KDF\(KDF\(<f3\(~k,.*', line): rank[75].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(~k,.*~sqn_root.*', line): rank[75].append(num)
    elif re.match('.*RcvS\(.*\'aia\'.*', line): rank[72].append(num)
    elif re.match('.*Commit\(.*', line): rank[70].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[70].append(num)
    elif re.match('.*RcvS\(.*', line): rank[69].append(num)
    elif re.match('.*!KU\( SHA256\(.*', line): rank[65].append(num)
    elif re.match('.*!KU\( KDF\(<f3\(~k, .*', line): rank[65].append(num)

elif lemma == "injectiveagreement_seaf_hss_kseaf_keyConf_noChanRev_noSqnRev_noSupiRev_noAsyKeyRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*=.*=.*=.*', line): rank[90].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[85].append(num)
    elif re.match('.*!KU\( f2\(~k.*', line) : rank[84].append(num)
    elif re.match('.*!KU\( f3\(~k.*', line) : rank[84].append(num)
    elif re.match('.*!KU\( f4\(~k.*', line) : rank[84].append(num)
    elif re.match('.*!KU\( f5\(~k.*', line) : rank[84].append(num)
    elif re.match('.*St_4_SEAF\(.*', line) : rank[80].append(num)
    elif re.match('.*St_3_SEAF\(.*', line) : rank[80].append(num)
    elif re.match('.*RcvS\(.*~idHN, ~idSN,.*\'aia\'.*', line): rank[72].append(num)
    elif re.match('.*CommitConf\(.*', line): rank[50].append(num)
    elif re.match('.*Commit\(.*', line): rank[50].append(num)
    elif re.match('.*RcvS\(.*~idHN, ~idSN,.*', line): rank[45].append(num)
    elif re.match('.*RcvS\(.*~idSN, ~idHN,.*', line): rank[45].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( f1\(~.*', line): rank[12].append(num)
    elif re.match('.*!KU\( f1\(K.*', line): rank[11].append(num)
    elif re.match('.*RcvS\(.*', line): rank[10].append(num)
    elif re.match('.*!KU\( SHA256\(.*', line): rank[9].append(num)
    elif re.match('.*!KU\( pk\(~sk.*', line): rank[7].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[6].append(num)
    elif re.match('.*!KU\( aenc\(<.*', line): rank[5].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[2].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[1].append(num)

elif lemma == "injectiveagreement_seaf_hss_kseaf_noChanRev" or \
     lemma == "injectiveagreement_seaf_hss_kseaf_noChanRev_noSqnRev_noSupiRev_noAsyKeyRev" or \
     lemma == "injectiveagreement_seaf_hss_kseaf_noRestr" or \
     lemma == "cleanAttack_injectiveagreement_seaf_hss_kseaf_noChanRev_noSqnRev_noSupiRev_noAsyKeyRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*=.*=.*=.*', line): rank[90].append(num)
    elif re.match('.*St_3_SEAF\(.*', line) : rank[80].append(num)
    elif re.match('.*RcvS\(.*', line): rank[72].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[60].append(num)
    elif re.match('.*Commit\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[30].append(num)

elif lemma == "injectiveagreement_ue_hss_kseaf_noRev" or \
     lemma == "noninjectiveagreement_ue_hss_kseaf_noRev" or \
     lemma == "noninjectiveagreement_ue_hss_snname_noRev":
  for line in lines:
    num = line.split(':')[0]
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!KU\( ~sk_HN.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*~sqn_root, ~sqn_root.*', line): rank[99].append(num)
    elif re.match('.*Sqn_HSS\(.*,.*,.*,.*,.* ~.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, \'1\',.*', line): rank[99].append(num)
    elif re.match('.*Sqn_UE\(.*, ~sqn_root, ~sqn_root,.*', line): rank[99].append(num)
    elif re.match('.*!HSS\(.*', line): rank[98].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[85].append(num)
    elif re.match('.*St_1_UE\(.*', line) or \
         re.match('.*St_1_SEAF\(.*', line) : rank[80].append(num)
    elif re.match('.*Sqn_UE\(.*, SqnUE, ~sqn_root, count.*', line): rank[76].append(num)
    elif re.match('.*Sqn_UE\(.*, \(\'1\'\+count\), ~sqn_root, count\.1.*', line): rank[76].append(num)
    elif re.match('.*Sqn_UE\(.*, \(\'1\'\+x\), ~sqn_root, count.*', line): rank[76].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[75].append(num)
    elif re.match('.*~~>.*', line): rank[73].append(num)
    elif re.match('.*RcvS\(.*', line): rank[72].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line) or \
	 re.match('.*!KD\( \(f5\(.*', line): rank[70].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[60].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[59].append(num)
    elif re.match('.*!KU\( ~supi.*', line): rank[51].append(num)
    elif re.match('.*!KU\( aenc\(.*', line): rank[50].append(num)


# EXECUTABILITY LEMMAS

elif lemma == "executability_honest":
  for line in lines:
    num = line.split(':')[0]  
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[99].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[99].append(num)
    elif re.match('.*RcvS\(.*', line): rank[98].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[90].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[90].append(num)
    elif re.match('.*!KU\( f5_star\(.*', line): rank[87].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[86].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[85].append(num)
    elif re.match('.*!KU\( f5\(~k.*', line): rank[84].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[83].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[72].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[60].append(num)
    elif re.match('.*!KD\( \(f5\(.*', line): rank[60].append(num)


elif lemma == "executability_resync" or \
     lemma == "executability_desync":
  for line in lines:
    num = line.split(':')[0]  
    if re.match('.*!KU\( ~k.*', line): rank[100].append(num)
    elif re.match('.*!HSS\(.*', line): rank[99].append(num)
    elif re.match('.*=.*=.*', line): rank[98].append(num)
    elif re.match('.*<.*=.*', line): rank[97].append(num)
    elif re.match('.*HSS_Resync_End\(.*', line): rank[96].append(num)
    elif re.match('.*!KU\( f5\(.*', line) or \
	 re.match('.*!KU\( f5_star\(.*', line): rank[95].append(num)
    elif re.match('.*!KU\( ~sqn_root.*', line): rank[95].append(num)
    elif re.match('.*St_1_UE\(.*', line): rank[94].append(num)
    elif re.match('.*St_1_HSS\(.*', line): rank[94].append(num)
    elif re.match('.*St_2_SEAF\(.*', line): rank[94].append(num)
    elif re.match('.*St_3_SEAF\(.*', line): rank[94].append(num)
    elif re.match('.*Sqn_UE\(.*', line): rank[93].append(num)
    elif re.match('.*Sqn_HSS\(.*', line): rank[93].append(num)
    elif re.match('.*~~>.*', line): rank[92].append(num)
    elif re.match('.*!Ltk_Sym\(.*', line): rank[90].append(num)
    elif re.match('.*RcvS\(.*', line): rank[70].append(num)
    elif re.match('.*!KU\( KDF\(.*', line): rank[60].append(num)
    elif re.match('.*!KU\( f3\(.*', line): rank[50].append(num)
    elif re.match('.*!KU\( f1_star\(.*', line): rank[40].append(num)
    elif re.match('.*!KU\( f1\(.*', line): rank[30].append(num)
    elif re.match('.*!KU\( \(f5\(.*', line): rank[20].append(num)
    elif re.match('.*!KD\( \(f5\(.*', line): rank[20].append(num)
    elif re.match('.*!KU\( \(f5_star\(.*', line): rank[20].append(num)
    elif re.match('.*!KD\( \(f5_star\(.*', line): rank[20].append(num)


else:
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    sys.stderr.write(goal)
    print goal

